ShouldBePi.agda:8,8-15
(x : _4) → _4 !=< One of type Set
when checking that the expression λ x → x has type One
